enrich
   file-id, 
   string
, 
   metadata
, 
   nat
with
   

   sorts directory-tree;
         entries-tree;
         stringdirectorytree;
   constants  ∅ : entries-tree;
   functions  dnode : metadata × entries-tree → directory-tree;
              fnode : fid → directory-tree;
              . [ . ] : entries-tree × string × directory-tree → entries-tree;
              . × . : string × directory-tree → stringdirectorytree;
              # . : entries-tree → nat;
              . -- . : entries-tree × string → entries-tree prio 9 left;
   predicates  . ∈ . : string × entries-tree;
               . ∈ . : stringdirectorytree × entries-tree;
               . ⊆ . : entries-tree × entries-tree;
   
   variables  sdt : entries-tree;
              sdt0 : entries-tree;
              sdt1 : entries-tree;
              sdt2 : entries-tree;
              tree : directory-tree;
              tree0 : directory-tree;
              tree1 : directory-tree;
              tree2 : directory-tree;
              md0 : metadata;
              fid0 : fid;
              str-tree : stringdirectorytree;
   partial functions  . [ . ] : entries-tree × string → directory-tree with λ sdt, str. str ∈ sdt;
   

   induction directory-tree, entries-tree generated by ∅, dnode, fnode, [ ];
             stringdirectorytree freely generated by ×;

   axioms disj :  ⊦ fnode(fid) ≠ dnode(md, sdt);
          used for: s, ls;
          fnode-inj :  ⊦ fnode(fid) = fnode(fid0) ↔ fid = fid0;
          used for: s, ls;
          dnode-inj :  ⊦ dnode(md, sdt) = dnode(md0, sdt0) ↔ md = md0 ∧ sdt = sdt0;
          used for: s, ls;
          Extension :  ⊦ sdt1 = sdt2 ↔ (∀ str. (str ∈ sdt1 ↔ str ∈ sdt2) ∧ sdt1[str] = sdt2[str]);
          used for: ls;
          In-empty :  ⊦ ¬ str ∈ ∅;
          used for: s, ls;
          In-insert :  ⊦ str ∈ sdt[str0, tree] ↔ str = str0 ∨ str ∈ sdt;
          used for: s, ls;
          In-store :  ⊦ str × tree ∈ sdt ↔ str ∈ sdt ∧ sdt[str] = tree;
          used for: s, ls;
          At-same :  ⊦ sdt[str, tree][str] = tree;
          used for: s, ls;
          At-other :  ⊦ str ≠ str0 → sdt[str0, tree][str] = sdt[str];
          used for: s, ls;
          Subset :  ⊦ sdt1 ⊆ sdt2 ↔ (∀ str. str ∈ sdt1 → str ∈ sdt2 ∧ sdt1[str] = sdt2[str]);
          used for: ls;
          Size-empty :  ⊦ # ∅ = 0;
          used for: s, ls;
          Size-insert :  ⊦ ¬ str ∈ sdt → # sdt[str, tree] = # sdt + 1;
          used for: s, ls;
          Del-in :  ⊦ str ∈ sdt -- str0 ↔ str ≠ str0 ∧ str ∈ sdt;
          used for: s, ls;
          Del-at :  ⊦ str ≠ str0 → (sdt -- str0)[str] = sdt[str];
          used for: s, ls;

   

   
end enrich